COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	proble[f84,jmc]		Towards a problem solving program
C00008 ENDMK
C⊗;
proble[f84,jmc]		Towards a problem solving program

We want a problem solving program that takes sentences in logic
as input and finds a tuple satisfying a condition.  We want the
domain of sentences to be such that whether there is a solution
and the set of solutions are computable.  The key to this is
that the axioms should force a finite domain of relevant elements.

Here's a part of the problem.  Everyone has a mother including
mothers.  Any domain closed under the  mother(x,y)  relation
is infinite.  Nevertheless, unless a problem has some special
characteristics, a person's mother, grandmother, etc. are
irrelevant.  Somehow the problem can be reduced to one with
a finite number of persons.

We want theorems of the form - Every model of a restriction of
the problem to a certain finite domain has an extension - or
none do.

The finite domain in question may be obtained by the circumscription
of a certain predicate.  For material objects, the predicate is often
  present(x), meaning that  x  is present in the situation.  Perhaps
it is  present(x,S0).

The circumscription should perhaps be performed ruthlessly, i.e.
taking into account only a subset of the facts at the risk of
error.

Consider the problem (I forget details) involving a box of matches,
a thumbtack and a candle.  Its solution involves using the matchbox
as a candle holder, fastening it to the wall with the thumbtack.
The psychological difficulty is that people tend to consider the
matchbox solely as a container for the matches.  We want our program
to be able to make this kind of error, i.e. to divide the constant
individuals into categories according to the normal role that this
kind of individual plays.

Here's an idea for relativization with respect to a predicate Dom.
We begin with a set of axioms.

Each existential quantification is left as is.
Each universal quantification  ∀x.E  is replaced by  ∀x.Dom(x) ⊃ E.
Unless we put everything into prenex form to begin with, equivalent
sets of axioms may give inequivalent relativizations.  Therefore,
distinguishing between positive an negative quantifiers is most likely
the right thing to do.  However, I wish to reserve judgment on this
point.  The effect of all this is to make objects that the axioms
assert to exist rather useless unless there is other evidence putting
them in the domain.  The applications may require elaborating this
to a sorted theory where there is a Dom  predicate for each sort.

Perhaps the opposite formula is also interesting, i.e. leave
universal formulas as is and replace existential formulas
by ∃x.Dom(x) ∧ ... .  This formula is stronger than the one
it replaces.  It amounts to saying that we will look for objects
only in Dom.

Here's an idea for making the notion of "essentially unary" more
precise.  Let  P(x,y,z)  be a ternary predicate and suppose that
we can show that there are just 7 possibilities for
the pair  (y,z)  and list them.  Then we can replace  P(x,y,z) by
P1(x) ∨ ... ∨ P7(x)  with suitable axioms for  P1,...P7.  This
eliminates the ternary predicate in favor of 7 unary predicates.

My solution to monadic predicate calculus involves converting an
arbitrary formula into a boolean combination of formulas whose
truth values can be assigned independently.  When else can this
be done?

The other approach says that the domain contains only a finite
number of kinds of individuals as characterized by the predicates.
But this is a subcase of the previous one, because the formulas
characterizing the kinds of individuals can then be assigned truth
valuse independently.  Well maybe this isn't obvious, so perhaps
in the non-monadic situation, these are different methods.